Nuprl Lemma : cons_interleaving2
4,23
postcript
pdf
T
:Type,
x
:
T
,
L
,
L1
,
L2
:
T
List. interleaving(
T
;
L1
;
L2
;
L
)
interleaving(
T
;
L1
;
x
.
L2
;
x
.
L
)
latex
Definitions
t
T
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
interleaving(
T
;
L1
;
L2
;
L
)
Lemmas
interleaving
wf
,
cons
interleaving
,
interleaving
symmetry
origin
T:Type, x:T, L, L1, L2:T List. interleaving(T;L1;L2;L) 
interleaving(T;L1;x.L2;x.L) T:Type, x:T, L, L1, L2:T List. interleaving(T;L1;L2;L) interleaving(T;L1;x.L2;x.L) 
T Q
Qx:A. B(x)